Nuprl Lemma : for_wf
2,24
postcript
pdf
A
,
B
,
C
:Type,
f
:(
B
C
C
),
k
:
C
,
as
:
A
List,
g
:(
A
B
). (For{
A
,
f
,
k
}
x
as
.
g
(
x
))
C
latex
Definitions
t
T
,
x
(
s
)
,
x
:
T
.
b
(
x
)
,
x
:
A
.
B
(
x
)
,
map(
f
;
as
)
,
reduce(
f
;
k
;
as
)
,
For{
T
,
op
,
id
}
x
as
.
f
(
x
)
Lemmas
reduce
wf
,
map
wf
origin
A, B, C:Type, f:(B
CC), k:C, as:A List, g:(AB). (For{A,f,k} x 
as. g(x)) C A, B, C:Type, f:(BCC), k:C, as:A List, g:(AB). (For{A,f,k} x as. g(x)) C T
x:T. b(x)x:A. B(x) as. f(x)